(set-logic QF_UFLRA)
(set-info :source |CPAchecker with bounded model checking on SV-COMP14 program using MathSAT5, submitted by Philipp Wendler, http://cpachecker.sosy-lab.org|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")


(define-fun _2 () Bool false)
(declare-fun ___pc@4 () Real)
(declare-fun __ADDRESS_OF____pc () Real)
(declare-fun |__ADDRESS_OF_main::data| () Real)
(declare-fun __BASE_ADDRESS_OF__ (Real) Real)
(declare-fun ___pc@3 () Real)
(declare-fun |main::data@2| () Real)
(define-fun _7 () Real 0)
(define-fun _8 () Real __ADDRESS_OF____pc)
(define-fun _9 () Real (__BASE_ADDRESS_OF__ _8))
(define-fun _10 () Bool (= _8 _9))
(define-fun _11 () Real ___pc@3)
(define-fun _12 () Bool (= _11 _7))
(define-fun _13 () Bool (and _10 _12))
(define-fun _14 () Real 17)
(define-fun _15 () Bool (= _11 _14))
(define-fun _18 () Bool (not _15))
(define-fun _19 () Bool (and _13 _18))
(define-fun _21 () Bool (and _12 _19))
(define-fun _24 () Real |__ADDRESS_OF_main::data|)
(define-fun _25 () Real (__BASE_ADDRESS_OF__ _24))
(define-fun _26 () Bool (= _24 _25))
(define-fun _27 () Real |main::data@2|)
(define-fun _28 () Bool (= _27 _7))
(define-fun _29 () Bool (and _26 _28))
(define-fun _30 () Bool (and _21 _29))
(define-fun _31 () Real 3)
(define-fun _32 () Real ___pc@4)
(define-fun _33 () Bool (= _32 _31))
(define-fun _34 () Bool (and _30 _33))
(declare-fun |__ADDRESS_OF_main::__CPAchecker_TMP_0| () Real)
(declare-fun |main::node@3| () Real)
(declare-fun |*(struct_node)*@3| (Real) Real)
(declare-fun |__ADDRESS_OF___VERIFIER_successful_alloc_*void#37| () Real)
(declare-fun |__ADDRESS_OF___VERIFIER_successful_alloc_*void#38| () Real)
(declare-fun |*(struct_list)*@2| (Real) Real)
(declare-fun ___pc@5 () Real)
(declare-fun |__ADDRESS_OF_main::node| () Real)
(declare-fun |main::__CPAchecker_TMP_0@3| () Real)
(declare-fun |*(struct_node)*@2| (Real) Real)
(declare-fun |__ADDRESS_OF_main::item| () Real)
(declare-fun |malloc#2| () Real)
(declare-fun |main::data@3| () Real)
(declare-fun |main::item@3| () Real)
(declare-fun |malloc#3| () Real)
(define-fun _35 () Bool (= _32 _14))
(define-fun _37 () Bool (not _35))
(define-fun _38 () Bool (and _34 _37))
(define-fun _49 () Real 10)
(define-fun _55 () Real 16)
(define-fun _61 () Real 9)
(define-fun _67 () Real 15)
(define-fun _73 () Real 8)
(define-fun _79 () Real 14)
(define-fun _85 () Real 7)
(define-fun _91 () Real 13)
(define-fun _97 () Real 6)
(define-fun _103 () Real 12)
(define-fun _109 () Real 5)
(define-fun _115 () Real 4)
(define-fun _189 () Real (- 1))
(define-fun _308 () Real |__ADDRESS_OF_main::__CPAchecker_TMP_0|)
(define-fun _309 () Real (__BASE_ADDRESS_OF__ _308))
(define-fun _310 () Bool (= _308 _309))
(define-fun _312 () Real |main::__CPAchecker_TMP_0@3|)
(define-fun _313 () Bool (= _312 _7))
(define-fun _316 () Bool (not _313))
(define-fun _318 () Real |__ADDRESS_OF_main::node|)
(define-fun _319 () Real (__BASE_ADDRESS_OF__ _318))
(define-fun _320 () Bool (= _318 _319))
(define-fun _322 () Real |malloc#2|)
(define-fun _323 () Bool (= _322 _7))
(define-fun _324 () Bool (not _323))
(define-fun _329 () Real |main::node@3|)
(define-fun _333 () Bool (= _329 _7))
(define-fun _336 () Bool (not _333))
(define-fun _339 () Real (|*(struct_node)*@2| _329))
(define-fun _340 () Bool (= _329 _339))
(define-fun _345 () Real |__ADDRESS_OF_main::item|)
(define-fun _346 () Real (__BASE_ADDRESS_OF__ _345))
(define-fun _347 () Bool (= _345 _346))
(define-fun _349 () Real |malloc#3|)
(define-fun _350 () Bool (= _349 _7))
(define-fun _351 () Bool (not _350))
(define-fun _355 () Real (- 8))
(define-fun _362 () Real |main::item@3|)
(define-fun _366 () Bool (= _362 _7))
(define-fun _369 () Bool (not _366))
(define-fun _371 () Real (|*(struct_node)*@3| _362))
(define-fun _372 () Bool (= _329 _371))
(define-fun _380 () Real (+ _362 _115))
(define-fun _381 () Real (|*(struct_list)*@2| _380))
(define-fun _3561 () Real |main::data@3|)
(define-fun _5204 () Bool (= _32 _7))
(define-fun _5207 () Bool (not _5204))
(define-fun _5208 () Bool (and _38 _5207))
(define-fun _5209 () Bool (= _32 _49))
(define-fun _5211 () Bool (not _5209))
(define-fun _5212 () Bool (and _5208 _5211))
(define-fun _5213 () Bool (= _32 _55))
(define-fun _5216 () Bool (not _5213))
(define-fun _5217 () Bool (and _5212 _5216))
(define-fun _5218 () Bool (= _32 _61))
(define-fun _5220 () Bool (not _5218))
(define-fun _5221 () Bool (and _5217 _5220))
(define-fun _5222 () Bool (= _32 _67))
(define-fun _5225 () Bool (not _5222))
(define-fun _5226 () Bool (and _5221 _5225))
(define-fun _5227 () Bool (= _32 _73))
(define-fun _5229 () Bool (not _5227))
(define-fun _5230 () Bool (and _5226 _5229))
(define-fun _5231 () Bool (= _32 _79))
(define-fun _5233 () Bool (not _5231))
(define-fun _5234 () Bool (and _5230 _5233))
(define-fun _5235 () Bool (= _32 _85))
(define-fun _5237 () Bool (not _5235))
(define-fun _5238 () Bool (and _5234 _5237))
(define-fun _5239 () Bool (= _32 _91))
(define-fun _5241 () Bool (not _5239))
(define-fun _5242 () Bool (and _5238 _5241))
(define-fun _5243 () Bool (= _32 _97))
(define-fun _5245 () Bool (not _5243))
(define-fun _5246 () Bool (and _5242 _5245))
(define-fun _5247 () Bool (= _32 _103))
(define-fun _5249 () Bool (not _5247))
(define-fun _5250 () Bool (and _5246 _5249))
(define-fun _5251 () Bool (= _32 _109))
(define-fun _5253 () Bool (not _5251))
(define-fun _5254 () Bool (and _5250 _5253))
(define-fun _5255 () Bool (= _32 _115))
(define-fun _5257 () Bool (not _5255))
(define-fun _5258 () Bool (and _5254 _5257))
(define-fun _5260 () Bool (and _33 _5258))
(define-fun _5263 () Bool (and _310 _5260))
(define-fun _5265 () Bool (and _316 _5263))
(define-fun _5266 () Bool (and _320 _5265))
(define-fun _5267 () Real |__ADDRESS_OF___VERIFIER_successful_alloc_*void#37|)
(define-fun _5268 () Real (ite _324 _5267 _7))
(define-fun _5269 () Bool (<= _5267 _7))
(define-fun _5270 () Bool (not _5269))
(define-fun _5271 () Bool (= _329 _5268))
(define-fun _5272 () Bool (and _5270 _5271))
(define-fun _5273 () Bool (and _5266 _5272))
(define-fun _5275 () Bool (and _336 _5273))
(define-fun _5276 () Bool (and _340 _5275))
(define-fun _5277 () Bool (and _347 _5276))
(define-fun _5278 () Real |__ADDRESS_OF___VERIFIER_successful_alloc_*void#38|)
(define-fun _5279 () Real (ite _351 _5278 _7))
(define-fun _5281 () Bool (<= _5267 _355))
(define-fun _5282 () Bool (not _5281))
(define-fun _5283 () Real (* (- 1) _5278))
(define-fun _5284 () Real (+ _5267 _5283))
(define-fun _5285 () Bool (<= _5284 _355))
(define-fun _5286 () Bool (and _5282 _5285))
(define-fun _5287 () Bool (= _362 _5279))
(define-fun _5288 () Bool (and _5286 _5287))
(define-fun _5289 () Bool (and _5277 _5288))
(define-fun _5291 () Bool (and _369 _5289))
(define-fun _5292 () Real (|*(struct_node)*@3| _5267))
(define-fun _5293 () Real (|*(struct_node)*@2| _5267))
(define-fun _5294 () Bool (= _5292 _5293))
(define-fun _5295 () Bool (and _372 _5294))
(define-fun _5296 () Bool (and _5291 _5295))
(define-fun _5297 () Bool (= _27 _381))
(define-fun _5298 () Bool (and _5296 _5297))
(define-fun _5299 () Bool (= _362 _3561))
(define-fun _5300 () Bool (and _5298 _5299))
(define-fun _5304 () Real ___pc@5)
(define-fun _5305 () Bool (= _5304 _31))
(define-fun _5306 () Bool (and _5300 _5305))
(declare-fun |inspect_before::shape@2| () Real)
(declare-fun |main::__CPAchecker_TMP_0@5| () Real)
(define-fun _391 () Real |inspect_before::shape@2|)
(define-fun _394 () Bool (= _391 _7))
(define-fun _3445 () Real |main::__CPAchecker_TMP_0@5|)
(define-fun _3446 () Bool (= _3445 _7))
(define-fun _5307 () Bool (= _5304 _14))
(define-fun _5309 () Bool (not _5307))
(define-fun _5310 () Bool (and _5306 _5309))
(define-fun _9087 () Bool (= _3561 _7))
(define-fun _9090 () Bool (not _9087))
(define-fun _9111 () Bool (= _391 _3561))
(define-fun _11207 () Bool (= _5304 _7))
(define-fun _11210 () Bool (not _11207))
(define-fun _11211 () Bool (and _5310 _11210))
(define-fun _11212 () Bool (= _5304 _49))
(define-fun _11214 () Bool (not _11212))
(define-fun _11215 () Bool (and _11211 _11214))
(define-fun _11216 () Bool (= _5304 _55))
(define-fun _11219 () Bool (not _11216))
(define-fun _11220 () Bool (and _11215 _11219))
(define-fun _11221 () Bool (= _5304 _61))
(define-fun _11223 () Bool (not _11221))
(define-fun _11224 () Bool (and _11220 _11223))
(define-fun _11225 () Bool (= _5304 _67))
(define-fun _11228 () Bool (not _11225))
(define-fun _11229 () Bool (and _11224 _11228))
(define-fun _11230 () Bool (= _5304 _73))
(define-fun _11232 () Bool (not _11230))
(define-fun _11233 () Bool (and _11229 _11232))
(define-fun _11234 () Bool (= _5304 _79))
(define-fun _11236 () Bool (not _11234))
(define-fun _11237 () Bool (and _11233 _11236))
(define-fun _11238 () Bool (= _5304 _85))
(define-fun _11240 () Bool (not _11238))
(define-fun _11241 () Bool (and _11237 _11240))
(define-fun _11242 () Bool (= _5304 _91))
(define-fun _11244 () Bool (not _11242))
(define-fun _11245 () Bool (and _11241 _11244))
(define-fun _11246 () Bool (= _5304 _97))
(define-fun _11248 () Bool (not _11246))
(define-fun _11249 () Bool (and _11245 _11248))
(define-fun _11250 () Bool (= _5304 _103))
(define-fun _11252 () Bool (not _11250))
(define-fun _11253 () Bool (and _11249 _11252))
(define-fun _11254 () Bool (= _5304 _109))
(define-fun _11256 () Bool (not _11254))
(define-fun _11257 () Bool (and _11253 _11256))
(define-fun _11258 () Bool (= _5304 _115))
(define-fun _11260 () Bool (not _11258))
(define-fun _11261 () Bool (and _11257 _11260))
(define-fun _11263 () Bool (and _5305 _11261))
(define-fun _11266 () Bool (and _310 _11263))
(define-fun _11267 () Bool (and _3446 _11266))
(define-fun _11366 () Bool (and _9090 _11267))
(define-fun _11375 () Bool (and _9111 _11366))
(define-fun _11376 () Bool (and _394 _11375))
(declare-fun |__ADDRESS_OF___VERIFIER_successful_alloc_*void#108| () Real)
(declare-fun |main::node@5| () Real)
(declare-fun |*(struct_list)*@3| (Real) Real)
(declare-fun *signed_int@3 (Real) Real)
(declare-fun |*(struct_node)*@5| (Real) Real)
(declare-fun |malloc#4| () Real)
(declare-fun |main::data@4| () Real)
(declare-fun ___pc@6 () Real)
(declare-fun |malloc#5| () Real)
(declare-fun *signed_int@2 (Real) Real)
(declare-fun |__ADDRESS_OF___VERIFIER_successful_alloc_*void#107| () Real)
(declare-fun |main::item@5| () Real)
(declare-fun |*(struct_node)*@4| (Real) Real)
(define-fun _16 () Real 1)
(define-fun _126 () Real 2)
(define-fun _397 () Bool (not _394))
(define-fun _400 () Real (+ _391 _115))
(define-fun _457 () Real 11)
(define-fun _3449 () Bool (not _3446))
(define-fun _3452 () Real |malloc#4|)
(define-fun _3453 () Bool (= _3452 _7))
(define-fun _3454 () Bool (not _3453))
(define-fun _3461 () Real |main::node@5|)
(define-fun _3465 () Bool (= _3461 _7))
(define-fun _3468 () Bool (not _3465))
(define-fun _3470 () Real (|*(struct_node)*@4| _3461))
(define-fun _3471 () Bool (= _3461 _3470))
(define-fun _3501 () Real |malloc#5|)
(define-fun _3502 () Bool (= _3501 _7))
(define-fun _3503 () Bool (not _3502))
(define-fun _3513 () Real |main::item@5|)
(define-fun _3517 () Bool (= _3513 _7))
(define-fun _3520 () Bool (not _3517))
(define-fun _3522 () Real (|*(struct_node)*@5| _3513))
(define-fun _3523 () Bool (= _3461 _3522))
(define-fun _3543 () Real (+ _3513 _115))
(define-fun _3544 () Real (|*(struct_list)*@3| _3543))
(define-fun _3580 () Real (|*(struct_list)*@2| _400))
(define-fun _3581 () Bool (= _3580 _7))
(define-fun _3584 () Bool (not _3581))
(define-fun _3590 () Real (|*(struct_node)*@3| _391))
(define-fun _3591 () Bool (= _3590 _7))
(define-fun _3594 () Bool (not _3591))
(define-fun _3617 () Real (|*(struct_node)*@3| _3590))
(define-fun _3618 () Bool (= _3617 _7))
(define-fun _3621 () Bool (not _3618))
(define-fun _9084 () Real |main::data@4|)
(define-fun _11268 () Bool (and _3449 _11266))
(define-fun _11269 () Bool (and _320 _11268))
(define-fun _11270 () Real |__ADDRESS_OF___VERIFIER_successful_alloc_*void#107|)
(define-fun _11271 () Real (ite _3454 _11270 _7))
(define-fun _11273 () Bool (<= _5278 _355))
(define-fun _11274 () Bool (not _11273))
(define-fun _11275 () Real (* (- 1) _11270))
(define-fun _11276 () Real (+ _5278 _11275))
(define-fun _11277 () Bool (<= _11276 _355))
(define-fun _11278 () Bool (and _11274 _11277))
(define-fun _11279 () Bool (= _3461 _11271))
(define-fun _11280 () Bool (and _11278 _11279))
(define-fun _11281 () Bool (and _11269 _11280))
(define-fun _11283 () Bool (and _3468 _11281))
(define-fun _11284 () Bool (= _3461 _11270))
(define-fun _11285 () Real (|*(struct_node)*@4| _11270))
(define-fun _11286 () Real (|*(struct_node)*@3| _11270))
(define-fun _11287 () Bool (= _11285 _11286))
(define-fun _11288 () Bool (or _11284 _11287))
(define-fun _11289 () Bool (= _3461 _5267))
(define-fun _11290 () Real (|*(struct_node)*@4| _5267))
(define-fun _11291 () Bool (= _5292 _11290))
(define-fun _11292 () Bool (or _11289 _11291))
(define-fun _11293 () Real (|*(struct_node)*@4| _5278))
(define-fun _11294 () Real (|*(struct_node)*@3| _5278))
(define-fun _11295 () Bool (= _11293 _11294))
(define-fun _11296 () Bool (and _11288 _11292))
(define-fun _11297 () Bool (and _11295 _11296))
(define-fun _11298 () Bool (and _3471 _11297))
(define-fun _11299 () Bool (and _11283 _11298))
(define-fun _11301 () Real (+ _11270 _115))
(define-fun _11302 () Real (*signed_int@3 _11301))
(define-fun _11303 () Real (*signed_int@2 _11301))
(define-fun _11304 () Bool (= _11302 _11303))
(define-fun _11305 () Bool (or _11284 _11304))
(define-fun _11307 () Real (+ _5267 _115))
(define-fun _11308 () Real (*signed_int@3 _11307))
(define-fun _11309 () Real (*signed_int@2 _11307))
(define-fun _11310 () Bool (= _11308 _11309))
(define-fun _11311 () Bool (or _11289 _11310))
(define-fun _11312 () Bool (and _11305 _11311))
(define-fun _11313 () Bool (and _11299 _11312))
(define-fun _11314 () Bool (and _347 _11313))
(define-fun _11315 () Real |__ADDRESS_OF___VERIFIER_successful_alloc_*void#108|)
(define-fun _11316 () Real (ite _3503 _11315 _7))
(define-fun _11318 () Bool (<= _11270 _355))
(define-fun _11319 () Bool (not _11318))
(define-fun _11320 () Real (* (- 1) _11315))
(define-fun _11321 () Real (+ _11270 _11320))
(define-fun _11322 () Bool (<= _11321 _355))
(define-fun _11323 () Bool (and _11319 _11322))
(define-fun _11324 () Bool (= _3513 _11316))
(define-fun _11325 () Bool (and _11323 _11324))
(define-fun _11326 () Bool (and _11314 _11325))
(define-fun _11328 () Bool (and _3520 _11326))
(define-fun _11329 () Bool (= _3513 _11315))
(define-fun _11330 () Real (|*(struct_node)*@5| _11315))
(define-fun _11331 () Real (|*(struct_node)*@4| _11315))
(define-fun _11332 () Bool (= _11330 _11331))
(define-fun _11333 () Bool (or _11329 _11332))
(define-fun _11334 () Bool (= _3513 _5278))
(define-fun _11335 () Real (|*(struct_node)*@5| _5278))
(define-fun _11336 () Bool (= _11293 _11335))
(define-fun _11337 () Bool (or _11334 _11336))
(define-fun _11338 () Real (|*(struct_node)*@5| _11270))
(define-fun _11339 () Bool (= _11285 _11338))
(define-fun _11340 () Real (|*(struct_node)*@5| _5267))
(define-fun _11341 () Bool (= _11290 _11340))
(define-fun _11342 () Bool (and _11333 _11337))
(define-fun _11343 () Bool (and _11339 _11342))
(define-fun _11344 () Bool (and _11341 _11343))
(define-fun _11345 () Bool (and _3523 _11344))
(define-fun _11346 () Bool (and _11328 _11345))
(define-fun _11347 () Bool (= _3544 _3561))
(define-fun _11349 () Real (+ _11315 _115))
(define-fun _11350 () Real (|*(struct_list)*@3| _11349))
(define-fun _11351 () Real (|*(struct_list)*@2| _11349))
(define-fun _11352 () Bool (= _11350 _11351))
(define-fun _11353 () Bool (or _11329 _11352))
(define-fun _11355 () Real (+ _5278 _115))
(define-fun _11356 () Real (|*(struct_list)*@3| _11355))
(define-fun _11357 () Real (|*(struct_list)*@2| _11355))
(define-fun _11358 () Bool (= _11356 _11357))
(define-fun _11359 () Bool (or _11334 _11358))
(define-fun _11360 () Bool (and _11353 _11359))
(define-fun _11361 () Bool (and _11347 _11360))
(define-fun _11362 () Bool (and _11346 _11361))
(define-fun _11363 () Bool (= _3513 _9084))
(define-fun _11364 () Bool (and _11362 _11363))
(define-fun _11377 () Bool (and _397 _11375))
(define-fun _11378 () Bool (and _3581 _11377))
(define-fun _11379 () Bool (and _3584 _11377))
(define-fun _11380 () Bool (and _394 _11379))
(define-fun _11381 () Bool (and _397 _11379))
(define-fun _11382 () Bool (and _3581 _11381))
(define-fun _11383 () Bool (and _3584 _11381))
(define-fun _11384 () Bool (and _3591 _11383))
(define-fun _11385 () Bool (and _3594 _11383))
(define-fun _11386 () Real ___pc@6)
(define-fun _11387 () Bool (= _11386 _115))
(define-fun _11388 () Bool (and _11385 _11387))
(define-fun _11389 () Bool (= _11386 _49))
(define-fun _11390 () Bool (and _11384 _11389))
(define-fun _11391 () Bool (or _11388 _11390))
(define-fun _11392 () Bool (= _11386 _97))
(define-fun _11393 () Bool (and _11382 _11392))
(define-fun _11396 () Bool (= _11386 _126))
(define-fun _11397 () Bool (and _11380 _11396))
(define-fun _11401 () Bool (and _394 _11378))
(define-fun _11402 () Bool (and _397 _11378))
(define-fun _11403 () Bool (and _3581 _11402))
(define-fun _11404 () Bool (and _3584 _11402))
(define-fun _11405 () Bool (= _11386 _109))
(define-fun _11406 () Bool (and _11404 _11405))
(define-fun _11411 () Bool (and _3591 _11403))
(define-fun _11412 () Bool (and _3594 _11403))
(define-fun _11413 () Bool (and _3618 _11412))
(define-fun _11414 () Bool (and _3621 _11412))
(define-fun _11415 () Bool (= _11386 _103))
(define-fun _11416 () Bool (and _11414 _11415))
(define-fun _11422 () Bool (= _11386 _457))
(define-fun _11423 () Bool (and _11411 _11422))
(define-fun _11430 () Bool (= _11386 _16))
(define-fun _11431 () Bool (and _11401 _11430))
(define-fun _11453 () Bool (= _11386 _31))
(define-fun _11454 () Bool (and _11364 _11453))
(define-fun _11455 () Bool (= _11386 _55))
(define-fun _11456 () Bool (and _11413 _11455))
(define-fun _11489 () Bool (or _11391 _11393))
(define-fun _11490 () Bool (or _11397 _11489))
(define-fun _11491 () Bool (or _11406 _11490))
(define-fun _11492 () Bool (or _11416 _11491))
(define-fun _11493 () Bool (or _11423 _11492))
(define-fun _11494 () Bool (or _11431 _11493))
(define-fun _11495 () Bool (or _11454 _11494))
(define-fun _11496 () Bool (or _11456 _11495))
(declare-fun |main::__CPAchecker_TMP_0@7| () Real)
(declare-fun |inspect_after::shape@2| () Real)
(define-fun _132 () Real 18)
(define-fun _1177 () Real |inspect_after::shape@2|)
(define-fun _1180 () Bool (= _1177 _7))
(define-fun _8950 () Real |main::__CPAchecker_TMP_0@7|)
(define-fun _8951 () Bool (= _8950 _7))
(define-fun _11439 () Bool (= _11386 _14))
(define-fun _11441 () Bool (not _11439))
(define-fun _11443 () Bool (and _11390 _11441))
(define-fun _11444 () Bool (and _11393 _11441))
(define-fun _11445 () Bool (and _11397 _11441))
(define-fun _11446 () Bool (and _11406 _11441))
(define-fun _11447 () Bool (and _11416 _11441))
(define-fun _11448 () Bool (and _11423 _11441))
(define-fun _11449 () Bool (and _11431 _11441))
(define-fun _11482 () Bool (and _11441 _11454))
(define-fun _11483 () Bool (and _11441 _11456))
(define-fun _16304 () Bool (= _9084 _7))
(define-fun _16307 () Bool (not _16304))
(define-fun _16329 () Bool (= _391 _9084))
(define-fun _17852 () Real (+ _3561 _115))
(define-fun _17867 () Bool (= _1177 _3561))
(define-fun _18533 () Bool (= _11386 _7))
(define-fun _18535 () Bool (not _18533))
(define-fun _18539 () Bool (not _11389))
(define-fun _18542 () Bool (not _11455))
(define-fun _18544 () Bool (= _11386 _61))
(define-fun _18547 () Bool (not _18544))
(define-fun _18549 () Bool (= _11386 _67))
(define-fun _18551 () Bool (not _18549))
(define-fun _18553 () Bool (= _11386 _73))
(define-fun _18555 () Bool (not _18553))
(define-fun _18557 () Bool (= _11386 _79))
(define-fun _18559 () Bool (not _18557))
(define-fun _18561 () Bool (= _11386 _85))
(define-fun _18563 () Bool (not _18561))
(define-fun _18565 () Bool (= _11386 _91))
(define-fun _18567 () Bool (not _18565))
(define-fun _18571 () Bool (not _11392))
(define-fun _18575 () Bool (not _11415))
(define-fun _18579 () Bool (not _11405))
(define-fun _18583 () Bool (not _11387))
(define-fun _18661 () Bool (and _11443 _18535))
(define-fun _18663 () Bool (and _11389 _18661))
(define-fun _18667 () Bool (and _11444 _18535))
(define-fun _18671 () Bool (and _18539 _18667))
(define-fun _18673 () Bool (and _18542 _18671))
(define-fun _18676 () Bool (and _18547 _18673))
(define-fun _18678 () Bool (and _18551 _18676))
(define-fun _18680 () Bool (and _18555 _18678))
(define-fun _18682 () Bool (and _18559 _18680))
(define-fun _18684 () Bool (and _18563 _18682))
(define-fun _18686 () Bool (and _18567 _18684))
(define-fun _18688 () Bool (and _11392 _18686))
(define-fun _18693 () Bool (and _11445 _18535))
(define-fun _18698 () Bool (and _18539 _18693))
(define-fun _18701 () Bool (and _18542 _18698))
(define-fun _18705 () Bool (and _18547 _18701))
(define-fun _18708 () Bool (and _18551 _18705))
(define-fun _18711 () Bool (and _18555 _18708))
(define-fun _18714 () Bool (and _18559 _18711))
(define-fun _18717 () Bool (and _18563 _18714))
(define-fun _18720 () Bool (and _18567 _18717))
(define-fun _18724 () Bool (and _18571 _18720))
(define-fun _18727 () Bool (and _18575 _18724))
(define-fun _18730 () Bool (and _18579 _18727))
(define-fun _18733 () Bool (and _18583 _18730))
(define-fun _18735 () Bool (not _11453))
(define-fun _18736 () Bool (and _18733 _18735))
(define-fun _18738 () Bool (and _11396 _18736))
(define-fun _18739 () Bool (not _11396))
(define-fun _18745 () Bool (and _11446 _18535))
(define-fun _18751 () Bool (and _18539 _18745))
(define-fun _18755 () Bool (and _18542 _18751))
(define-fun _18760 () Bool (and _18547 _18755))
(define-fun _18764 () Bool (and _18551 _18760))
(define-fun _18768 () Bool (and _18555 _18764))
(define-fun _18772 () Bool (and _18559 _18768))
(define-fun _18776 () Bool (and _18563 _18772))
(define-fun _18780 () Bool (and _18567 _18776))
(define-fun _18785 () Bool (and _18571 _18780))
(define-fun _18789 () Bool (and _18575 _18785))
(define-fun _18792 () Bool (and _11405 _18789))
(define-fun _18799 () Bool (and _11447 _18535))
(define-fun _18806 () Bool (and _18539 _18799))
(define-fun _18811 () Bool (and _18542 _18806))
(define-fun _18817 () Bool (and _18547 _18811))
(define-fun _18822 () Bool (and _18551 _18817))
(define-fun _18827 () Bool (and _18555 _18822))
(define-fun _18832 () Bool (and _18559 _18827))
(define-fun _18837 () Bool (and _18563 _18832))
(define-fun _18842 () Bool (and _18567 _18837))
(define-fun _18848 () Bool (and _18571 _18842))
(define-fun _18852 () Bool (and _11415 _18848))
(define-fun _18860 () Bool (and _11448 _18535))
(define-fun _18868 () Bool (and _18539 _18860))
(define-fun _18874 () Bool (and _18542 _18868))
(define-fun _18881 () Bool (and _18547 _18874))
(define-fun _18887 () Bool (and _18551 _18881))
(define-fun _18893 () Bool (and _18555 _18887))
(define-fun _18899 () Bool (and _18559 _18893))
(define-fun _18905 () Bool (and _18563 _18899))
(define-fun _18911 () Bool (and _18567 _18905))
(define-fun _18918 () Bool (and _18571 _18911))
(define-fun _18924 () Bool (and _18575 _18918))
(define-fun _18929 () Bool (and _18579 _18924))
(define-fun _18933 () Bool (and _18583 _18929))
(define-fun _18935 () Bool (and _18735 _18933))
(define-fun _18938 () Bool (and _18739 _18935))
(define-fun _18939 () Bool (= _11386 _132))
(define-fun _18941 () Bool (not _18939))
(define-fun _18942 () Bool (and _18938 _18941))
(define-fun _18945 () Bool (not _11430))
(define-fun _18946 () Bool (and _18942 _18945))
(define-fun _18954 () Bool (and _11449 _18535))
(define-fun _18963 () Bool (and _18539 _18954))
(define-fun _18970 () Bool (and _18542 _18963))
(define-fun _18978 () Bool (and _18547 _18970))
(define-fun _18985 () Bool (and _18551 _18978))
(define-fun _18992 () Bool (and _18555 _18985))
(define-fun _18999 () Bool (and _18559 _18992))
(define-fun _19006 () Bool (and _18563 _18999))
(define-fun _19013 () Bool (and _18567 _19006))
(define-fun _19021 () Bool (and _18571 _19013))
(define-fun _19028 () Bool (and _18575 _19021))
(define-fun _19034 () Bool (and _18579 _19028))
(define-fun _19039 () Bool (and _18583 _19034))
(define-fun _19042 () Bool (and _18735 _19039))
(define-fun _19046 () Bool (and _18739 _19042))
(define-fun _19048 () Bool (and _18941 _19046))
(define-fun _19050 () Bool (and _11430 _19048))
(define-fun _19077 () Bool (and _11482 _18535))
(define-fun _19078 () Bool (and _18539 _19077))
(define-fun _19080 () Bool (and _18542 _19078))
(define-fun _19081 () Bool (and _18547 _19080))
(define-fun _19083 () Bool (and _18551 _19081))
(define-fun _19084 () Bool (and _18555 _19083))
(define-fun _19085 () Bool (and _18559 _19084))
(define-fun _19086 () Bool (and _18563 _19085))
(define-fun _19087 () Bool (and _18567 _19086))
(define-fun _19088 () Bool (and _18571 _19087))
(define-fun _19089 () Bool (and _18575 _19088))
(define-fun _19090 () Bool (and _18579 _19089))
(define-fun _19091 () Bool (and _18583 _19090))
(define-fun _19092 () Bool (and _11453 _19091))
(define-fun _19094 () Bool (and _310 _19092))
(define-fun _19095 () Bool (and _8951 _19094))
(define-fun _19208 () Bool (and _16307 _19095))
(define-fun _19228 () Bool (and _16329 _19208))
(define-fun _19229 () Bool (and _394 _19228))
(define-fun _19401 () Bool (and _11483 _18535))
(define-fun _19415 () Bool (and _18539 _19401))
(define-fun _19429 () Bool (and _11455 _19415))
(define-fun _19431 () Real (|*(struct_list)*@2| _17852))
(define-fun _19432 () Bool (= _19431 _7))
(define-fun _19434 () Bool (and _19429 _19432))
(define-fun _19446 () Bool (and _17867 _19434))
(define-fun _19447 () Bool (and _1180 _19446))
(define-fun _19471 () Bool (or _18663 _18688))
(define-fun _19472 () Bool (or _18738 _19471))
(define-fun _19473 () Bool (or _18792 _19472))
(define-fun _19474 () Bool (or _18852 _19473))
(define-fun _19475 () Bool (or _18946 _19474))
(define-fun _19476 () Bool (or _19050 _19475))
(define-fun _19477 () Bool (or _19229 _19476))
(define-fun _19478 () Bool (or _19447 _19477))


(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _34)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert _2)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _5306)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert _11376)
(set-info :status unsat)
(check-sat)
(pop 1)
(push 1)
(assert _11496)
(set-info :status sat)
(check-sat)
(pop 1)
(push 1)
(assert _19478)
(set-info :status sat)
(check-sat)
(pop 1)
(exit)
